﻿// --------------------------------------------------------------------------------------------------------------------
// <copyright file="Examples.cs" company="Team Awesome">
//   Awesome
// </copyright>
// <summary>
//   
// </summary>
// --------------------------------------------------------------------------------------------------------------------

namespace System.Collections.CodeContractExamples
{
	using Diagnostics.Contracts;

	/// <summary>
	/// Examples where Code Contracts could be better.
	/// </summary>
	public static class Examples
	{
		/// <summary>
		/// This can only be changed through a public method.
		/// </summary>
		private static bool _isTrue = true;

		/// <summary>
		/// Code Contracts can't prove this ensures if ReturnTrue does not have an ensure that states the same.
		/// </summary>
		/// <returns>
		/// The some test.
		/// </returns>
		public static int SomeTest()
		{
			Contract.Ensures(Contract.Result<int>() > 0);

			if (ReturnTrue())
				return 1;
			return -1;
		}

		/// <summary>
		/// Always return true.
		/// </summary>
		/// <returns>
		/// Returns true.
		/// </returns>
		private static bool ReturnTrue()
		{
			// If this is commented, then the Code Contracts will have no clue about the returns of this method.
			Contract.Ensures(Contract.Result<bool>());

			return true;
		}

		/// <summary>
		/// Sets _isTrue to false
		/// </summary>
		public static void SetIsTrueToFalse()
		{
			_isTrue = false;
		}
		
		/// <summary>
		/// Fails if SetIsTrueToFalse is called before this. Unreachable by Pex because _isTrue is a private field.
		/// </summary>
		/// <returns>
		/// The cannot be covered by Pex.
		/// </returns>
		public static bool CannotBeCoveredByPex()
		{
			if (!_isTrue)
				throw new Exception("FAIL");
			return true;
		}
	}
}